COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	THE FRAME PROBLEM CONSIDERED AS A CIRCUMSCRIPTION PROBLEM
C00007 00003	NEW APPROACH
C00009 ENDMK
C⊗;
THE FRAME PROBLEM CONSIDERED AS A CIRCUMSCRIPTION PROBLEM

	This is a first attempt at applying circumscription induction
to the frame problem.  We would like to get the result that unmoved
blocks don't change their positions by applying circumscription induction
to the rule describing the change of position of a moved block.
More generally, we have a collection A of sentences that determine that
certain objects are moved - some are moved directly, some move because
they are attached to objects that move, and some move as consequences
of more abstruse laws, e.g. they become unsupported and fall or are
struck by moving objects.  We want to apply circumscription to A
and conclude (conjecturally) that those objects which are not required
to move in consequence of A stay where they were.
If we omit a cause of motion from the set of sentences, then we will
wrongly conclude that an object doesn't move.  This is the way it should
be.

	Here is a variant that works in some simple cases, though it is
not yet clear what reasoning motivates the application of circumscription
in precisely this way.  We have

(1)	on(x,p,move(x,p,s)).

Notice that we are writing it as a free variable formula rather than
in the form ∀x p s.on(x,p,move(x,p,s)).  What we want the circumscription
schema to express is that the only things whose position (what they are on)
can change are those whose changing follows from (1).
We write

(2)	P(y) ≡ ∃q.¬(on(y,q,move(x,p,s)) ≡ on(y,q,s))

to express that y is moved when x is moved to p.


	Choosing Q as a predicate parameter, the following formula
has the right consequences if it is taken as the circumscription formula:

(3)	Q(x) ∧ on(x,p,move(x,p,s)) ⊃ ∀y.(P(y) ⊃ Q(y)).

We need only take

(4)	Q(y) ≡ y = x

and substitute for P from (2), getting

(5)	x = x ∧ on(x,p,move(x,p,s)) ⊃ ∀y.(∃q.¬(on(y,q,move(x,p,s)) ≡ on(y,q,s))
		⊃ y = x),

which converts to

(6)	on(x,p,move(x,p,s)) ⊃ ∀y.(y ≠ x ⊃ ∀q.(on(y,q,move(x,p,s)) ≡ on(y,q,s))),

when we replace the second implication by its contrapositive.  Since the
premise of (6) is an axiom, we get

(7)	∀y.(y ≠ x ⊃ ∀q.(on(y,q,move(x,p,s)) ≡ on(y,q,s))),

which is the desired frame axiom.

	As stated above, this way of applying circumscription gives the
desired answer, but it is not clear what general principle is being
appealed to.  Applying circumscription to formulas with free variables
in them didn't come up previously.


Gluing

	Now we attempt to meet a challenge from Bob Filman to allow for
one block glued to another.  Suppose we change (1) to

(8)	on(x,p,move(x,p,s)) ∧ ∀z.(glued(z,x) ⊃ on(z,p,move(x,p,s))),

and again use the P(x) given by (2).  The circumscription induction
formula is

(9) Q(x) ∧ on(x,p,move(x,p,s)) ∧ ∀z.((¬P(z) ∨ Q(z)) ⊃ (glued(z,x) >
on(z,p,move(x,p,s)))) ⊃ ∀y.(P(y) ⊃ Q(y)).

NEW APPROACH

∀x e s.((¬∃c.moves(c,x,e,s)) ⊃ location(x,result(e,s)) = location(x,s))

If no cause c moves the object x when event e occurs in situation s, then
the location of x in the situation that results from s is the same as the
location of x in situation s.  This is the general law that says that
something moves only when something moves it.

∀p x pl s.moves(move(p,x,pl),x,move(p,x,pl),s)

A person p moving an object x to a place pl in situation s moves the object
x when the even of moving the object occurs in situation s.
This is the law that says that the event of moving something moves it.
The form it takes is partly determined by the fact that it has to work
with the previous law.

∀p x pl s.(location(x,result(move(p,x,pl),s) = pl)

This is the active form of the law that says that an object goes to where
it is moved.

Now suppose we have the following special facts

location(A,s0) = B

location(B,s0) = Table

Now let us apply circumscription to the above collection of facts.
From it we should be able to deduce

location(A,result(move(John,A,C),s0)) = C

and

location(B,result(move(John,A,C),s0)) = Table

and

location(Table,result(move(John,A,C),s0)) = location(Table,s0).